Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		from(X)	→ cons(X,n__from(s(X)))
2:		2ndspos(0,Z)	→ rnil
3:		2ndspos(s(N),cons(X,n__cons(Y,Z)))	→ rcons(posrecip(activate(Y)),2ndsneg(N,activate(Z)))
4:		2ndsneg(0,Z)	→ rnil
5:		2ndsneg(s(N),cons(X,n__cons(Y,Z)))	→ rcons(negrecip(activate(Y)),2ndspos(N,activate(Z)))
6:		pi(X)	→ 2ndspos(X,from(0))
7:		plus(0,Y)	→ Y
8:		plus(s(X),Y)	→ s(plus(X,Y))
9:		times(0,Y)	→ 0
10:		times(s(X),Y)	→ plus(Y,times(X,Y))
11:		square(X)	→ times(X,X)
12:		from(X)	→ n__from(X)
13:		cons(X1,X2)	→ n__cons(X1,X2)
14:		activate(n__from(X))	→ from(X)
15:		activate(n__cons(X1,X2))	→ cons(X1,X2)
16:		activate(X)	→ X

There are 15 dependency pairs:


17:		FROM(X)	→ CONS(X,n__from(s(X)))
18:		2ndspos#(s(N),cons(X,n__cons(Y,Z)))	→ ACTIVATE(Y)
19:		2ndspos#(s(N),cons(X,n__cons(Y,Z)))	→ 2ndsneg#(N,activate(Z))
20:		2ndspos#(s(N),cons(X,n__cons(Y,Z)))	→ ACTIVATE(Z)
21:		2ndsneg#(s(N),cons(X,n__cons(Y,Z)))	→ ACTIVATE(Y)
22:		2ndsneg#(s(N),cons(X,n__cons(Y,Z)))	→ 2ndspos#(N,activate(Z))
23:		2ndsneg#(s(N),cons(X,n__cons(Y,Z)))	→ ACTIVATE(Z)
24:		PI(X)	→ 2ndspos#(X,from(0))
25:		PI(X)	→ FROM(0)
26:		PLUS(s(X),Y)	→ PLUS(X,Y)
27:		TIMES(s(X),Y)	→ PLUS(Y,times(X,Y))
28:		TIMES(s(X),Y)	→ TIMES(X,Y)
29:		SQUARE(X)	→ TIMES(X,X)
30:		ACTIVATE(n__from(X))	→ FROM(X)
31:		ACTIVATE(n__cons(X1,X2))	→ CONS(X1,X2)

The approximated dependency graph contains 3 SCCs: {26}, {28} and {19,22}.

Consider the SCC {26}. There are no usable rules. By taking the AF π with π(PLUS) = 1 together with the lexicographic path order with empty precedence, rule 26 is strictly decreasing.

Consider the SCC {28}. There are no usable rules. By taking the AF π with π(TIMES) = 1 together with the lexicographic path order with empty precedence, rule 28 is strictly decreasing.

Consider the SCC {19,22}. The usable rules are {1,12-16}. By taking the AF π with π(2ndsneg#) = π(2ndspos#) = π(activate) = π(cons) = π(from) = π(n__cons) = π(n__from) = 1 together with the lexicographic path order with empty precedence, the rules in {1,12-16} are weakly decreasing and the rules in {19,22} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (1.04 seconds) --- May 4, 2006